(set-logic QF_BV)
(set-info :source |
    Oliver Wienand, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, 
    Gert-Martin Greuel: An Algebraic Approach for Proving Data Correctness
    in Arithmetic Data Paths. CAV 2008: 473-486
    <http://www.springerlink.com/content/16532l8178178042/>
|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unknown)
(declare-fun var2 () (_ BitVec 32))
(declare-fun var3 () (_ BitVec 32))
(declare-fun var4 () (_ BitVec 32))
(declare-fun var8 () (_ BitVec 65))
(declare-fun var10 () (_ BitVec 65))
(declare-fun var12 () (_ BitVec 65))
(declare-fun var14 () (_ BitVec 65))
(declare-fun var17 () (_ BitVec 65))
(declare-fun var19 () (_ BitVec 65))
(declare-fun var23 () (_ BitVec 65))
(declare-fun var31 () (_ BitVec 65))
(declare-fun var32 () (_ BitVec 1))
(declare-fun var33 () (_ BitVec 1))
(declare-fun var34 () (_ BitVec 1))
(declare-fun property () (_ BitVec 1))
(declare-fun Fresh__0 () (_ BitVec 1))
(declare-fun Fresh__1 () (_ BitVec 1))
(assert (= var8 (concat (_ bv0 33) var4)))
(assert (= var10 (concat (_ bv0 33) var2)))
(assert (= var12 (bvmul var8 var10)))
(assert (= var14 (concat (_ bv0 33) var3)))
(assert (= var17 (bvmul var10 var14)))
(assert (= var19 (bvadd var12 var17)))
(assert (= var23 (bvadd var8 var14)))
(assert (= var31 (bvmul var10 var23)))
(assert (= (= Fresh__0 (_ bv1 1)) (= var19 var31)))
(assert (= var32 Fresh__0))
(assert (= var33 (bvnot (_ bv1 1))))
(assert (= var34 (bvor var32 var33)))
(assert (= property ((_ extract 0 0) var34)))
(assert (= (= Fresh__1 (_ bv1 1)) (= property (_ bv0 1))))
(assert (= (_ bv1 1) Fresh__1))
(check-sat)
(exit)
